FDL - Nuprl Definition : antecedent-function

Nuprl Definition : antecedent-function

11,40

P ==

e:{e:E| P(e)} . (f(e) < e) & Q(f(e))

clarification:

antecedent-function(es;P;Q;f) ==

e:{e:es-E(es)| P(e)} . es-causl(es; (f(e)); e) & Q(f(e))

Definitions x:A. B(x), {x:A| B(x)} , E, P & Q, (e < e'), f(a)

FDL editor aliases antecedent-function

Definitions	x:A. B(x), {x:A\| B(x)} , E, P & Q, (e < e'), f(a)
FDL editor aliases	antecedent-function